Implement Option A from design-formal-semantics-for-laurel-ir.md: a
standalone big-step operational semantics for all ~35 Laurel StmtExpr
constructors, independent of Core semantics.

New files:
- Strata/Languages/Laurel/LaurelSemantics.lean: Core semantic definitions
  including LaurelValue, LaurelStore, LaurelHeap, Outcome types, and
  mutually inductive EvalLaurelStmt/EvalLaurelBlock relations covering
  literals, variables, primitive operations, control flow (if/while/
  block/exit/return), assignments, verification constructs (assert/
  assume), static calls, OO features (new/field select/instance call/
  reference equals/is type/as type), and specification constructs
  (forall/exists/old/fresh/assigned/prove by/contract of).

- Strata/Languages/Laurel/LaurelSemanticsProps.lean: Properties including
  store monotonicity (UpdateStore/InitStore preserve definedness),
  store operation determinism, catchExit properties, evalPrimOp
  determinism, and block value semantics. Full evaluation determinism
  theorem is stated but admitted (requires mutual induction).

- StrataTest/Languages/Laurel/LaurelSemanticsTest.lean: 30+ concrete
  evaluation tests covering literals, identifiers, primitive ops (add,
  and, not, lt, strconcat), blocks (empty, singleton, multi-statement),
  if-then-else (true/false/no-else), exit (propagation, labeled catch,
  non-matching), return (with/without value, short-circuit), local
  variables (init/uninit), assert/assume, prove-by, nested control
  flow, and evalPrimOp/catchExit unit tests.

- docs/designs/design-formal-semantics-for-laurel-ir.md: Design document
  describing three options (A: direct, B: shallow, C: hybrid) with
  recommendation for Option C. This implementation is Option A, serving
  as a reference semantics for translation correctness proofs.

Design decisions:
- Outcome type explicitly models non-local control flow (exit/return)
- EvalArgs uses the expression evaluator δ (non-mutual) for call
  argument evaluation, avoiding Lean 4 mutual inductive limitations
- Heap model is separate from store for OO features
- Specification constructs (forall, exists, old, fresh, assigned,
  contract_of) are delegated to the expression evaluator δ
- Static/instance calls restore the caller store after body evaluation

Known limitations:
- Determinism theorem is admitted (sorry) - requires careful mutual
  induction over EvalLaurelStmt/EvalLaurelBlock
- While loop semantics only captures terminating executions (inductive)
- Call argument evaluation uses δ rather than full EvalLaurelStmt
  (avoids mutual inductive nesting issues in Lean 4)
- Translation correctness proof is out of scope (separate task)

Add HeapFieldWrite_deterministic and EvalArgs_deterministic lemmas to
LaurelSemanticsProps.lean as building blocks for the full
EvalLaurelStmt determinism proof.

HeapFieldWrite_deterministic: given the same heap, address, field, and
value, the resulting heap is unique. Proof by funext and by_cases on
address equality.

EvalArgs_deterministic: given the same evaluator, store, and expression
list, the resulting value list is unique. Proof by induction on the
first derivation, using functionality of the pure evaluator δ.

AllocHeap_deterministic is NOT included because AllocHeap is
non-deterministic in the allocated address — the constructor
existentially picks any addr where h addr = none, so two derivations
can choose different addresses. The full EvalLaurelStmt determinism
proof will need either a weaker formulation (heap bisimilarity up to
address renaming) or AllocHeap must be made deterministic (e.g., pick
the smallest free address).

Design ref: docs/designs/design-formal-semantics-for-laurel-ir.md
Chosen design: Option A (Direct Semantics) — auxiliary lemmas for
sub-relations to support the main determinism theorem.